Interval analysis is but one technique used to determine static lower and upper bounds on values of computer program variables. While these determined interval bounds are useful—especially for inferring invariants to prove buffer overflow checks—they nevertheless are inadequate as invariants due to a lack of relational information among the variables.
Abstract Interpretation (see Patrick Cousot & Radhia Cousot, ACM Principles of Programming Languages, 1977) is a framework that allows us to analyze programs to infer useful information such as intervals for variables. An abstract interpretation over a program requires us to define some basic components in a mathematically well-defined way to carry out program analysis automatically. By the way of further background, commercial as well as freely available tools such as F-Soft(NEC Laboratories America), Astree(Airbus Inc.), PolySpace(Mathworks Inc.) and CodeSonar(GrammaTech Inc.) implement the generic abstract interpretation algorithm. To instantiate such frameworks, we need to arrive at suitable representation (abstract domain objects) and algorithms to perform the following mathematical operations on the representation: (a) Join, (b)Intersection, (c)Transfer Function, (d) Projection, (e) Widening, (f) Narrowing and (g) Inclusion check.
Any mathematically sound (see e.g., Patrick Cousot & Radhia Cousot, “Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints”, ACM Principles of Programming Languages, pp. 238-252, 1977.) definition of the representation accompanied by algorithms to carry out operations (a-f) described above constitute a mathematically sound abstract domain. Such domains can be used as black-boxes by the frameworks mentioned above to perform useful program analysis tasks oriented towards program verification, optimization and other applications of this framework.
Interval Ranges (see, e.g., Patrick Cousot & Radhia Cousot, “Static Determination of Dynamic Properties of Program”, Proceedings of the Second International Symposium on Programming, pp. 106-130, 1976), Polyhedra (see, e.g., Patrick Cousot & Nicholas Halbwachs, “Automatic Discovery of linear restraints among the variables of a program”, ACM Principles of Programming Languages, pp 84-97, 1979) and Octagons (see Antoine Mine, PhD Thesis, Ecole Normale Superiure, 2005) are examples of abstract domains that provide representations and algorithms sufficient to carry out abstract interpretation. They are targeted towards buffer overflow detection by computing variable ranges but can be applicable to other applications as well.